horn description logic
First Order-Rewritability and Containment of Conjunctive Queries in Horn Description Logics
We study FO-rewritability of conjunctive queries in the presence of ontologies formulated in a description logic between EL and Horn-SHIF, along with related query containment problems. Apart from providing characterizations, we establish complexity results ranging from ExpTime via NExpTime to 2ExpTime, pointing out several interesting effects. In particular, FO-rewriting is more complex for conjunctive queries than for atomic queries when inverse roles are present, but not otherwise.
Finite Model Reasoning in Horn Description Logics
García, Yazmín Ibáñez (Free University of Bozen-Bolzano) | Lutz, Carsten (University of Bremen) | Schneider, Thomas (University of Bremen)
We study finite model reasoning in expressive Horn description logics (DLs), starting with a reduction of finite ABox consistency to unrestricted ABox consistency. The reduction relies on reversing certain cycles in the TBox, an approach that originated in database theory, was later adapted to the inexpressive DL DL-Lite_F , and is shown here to extend to the expressive Horn DL Horn-ALCFI . The model construction used to establish correctness makes the structure of finite models more explicit than existing approaches to finite model reasoning in expressive DLs that rely on solving systems of inequations over the integers. Since the reduction incurs an exponential blow-up, we then develop a dedicated consequence-based algorithm for finite ABox consistency in Horn-ALCFI that implements the reduction on-the-fly rather than executing it up-front. The algorithm has optimal worst-case complexity and provides a promising foundation for implementations. We next show that our approach can be adapted to finite (positive existential) query answering relative to Horn-ALCFI TBoxes, proving that this problem is EXPTIME-complete in combined complexity and PTIME-complete in data complexity. For finite satisfiability and subsumption, we also show that our techniques extend to Horn-SHIQ.
First-Order Rewritability of Atomic Queries in Horn Description Logics
Bienvenu, Meghyn (CNRS and Université Paris Sud) | Lutz, Carsten (University of Bremen) | Wolter, Frank (University of Liverpool)
One of the most advanced approaches to querying data in the presence of ontologies is to make use of relational database systems, rewriting the original query and the ontology into a new query that is formulated in SQL or, equivalently, in first-order logic (FO). For ontologies written in many standard description logics (DLs), however, such FO-rewritings are not guaranteed to exist. We study FO-rewritings and their existence for a basic class of queries and for ontologies formulated in Horn DLs such as Horn-SHI and EL. Our results include characterizations of the existence of FO-rewritings, tight complexity bounds for deciding whether an FO-rewriting exists (ExpTime and PSpace), and tight bounds on the (worst-case) size of FO-rewritings, when presented as a union of conjunctive queries.